Notes (Week 5 Monday)

Natural deduction!

It's a formal proof system for predicate logic.

A formal proof system is a set of *inference rules*
 that tell you how you're allowed to build proofs
 from other proofs.
Alternatively: how you're allowed to draw conclusions
 from premises.

Generally rules take this form:

  premise    premise  ...
  _________________________ name
        conclusion

Intuitively: if you have proofs of all the premises,
 you can invoke the rule "name" to conclude "conclusion".

The point is:
  the *only* proof steps we allow are those that
  are instances of one of the inference rules.

This makes the proof easy to check for correctness:
  we just check if every rule application looks
  like the inference rule we claim to apply
  (simple syntactic check)

But: getting the intution of *why* a claim is true
  from a ND proof might be hard.

→-introduction:

   [A]
    .
    .
    B
  ______ →-I
  A → B

 "If I can prove B under the assumption that A holds,
  then I can prove A → B"

Alternative notation:

  ⊢ A → B

  ⊢ provability

   ⊢ φ "I have a natural deduction proof of φ"

   T ⊢ φ "I have a natural deduction proof of φ,
          from the premises T"     

   A ⊢ B
 __________ →-I
  ⊢ A → B

 Premises in square brackets denote
  "local" premises that only exist in a subproof

Q: Is there a good way to specify the scope of the premise?
A: Not in this notation :(
   But see Fitch notation (later)


B ∧ A          B ∧ A
_____  ∧-E     ______  ∧-E
  A             B
 ____________________  ∧-I
  A ∧ B


The above is a proof of commutativity of ∧
formally:

     B ∧ A    ⊢    A ∧ B

Fitch style rules are more vertical than horizontal

1 | premise
2 | premise
3 |-
4 | conclusion   (justification)

Generally: a proof proceeds by going from premises
 (at the top) and using inference rules (one per line)
 to conclude more and more thing

∧-I

| A
| B
|-
| A ∧ B     ∧-I


→-introduction:

   [A]
    .
    .
    B
  ______ →-I
  A → B


| | A
| |-
| | B
|-
| A → B   →-I

c.f. programming languages (Python)

Q: Are we allowed to use the ND proof checker in assignments?
A: Yes! Feel free to use it in assignments and exams.


Q: If you're using other "obvious" rules, do you have to derive them
   or can you assume them? (in e.g. exam situations)
A: Hopefully the question text should make this clear.
    (but A1 doesn't :( )
   By default: feel free to use any of the derived rules from either:
    - the slides, or
    - the sidebar of the ND proof editor


We have defined:

   ⊢   provabilitiy

   T ⊢ φ  means "we have an ND proof of φ from the premises in T"


   ⊧   "models", truth

   T ⊧ φ  means "in every model that satisfies T, φ is satisfied"
             ⟦φ⟧v

We now have the infrastructure to ask these questions:

  are the things we can prove in fact true?
   (soundess)

   If T ⊢ φ  then T ⊧ φ

  are the things that are true in fact provable?
   (completeness)

   If T ⊧ φ then T ⊢ φ

You can think of universal quantification
  (over finite domains) as syntactic sugar
  for conjunction


  ∀x∈{a,b,c}. P(x)   ≡  P(a) ∧ P(b) ∧ P(c)


We're specifically doing *first-order* predicate logic.
 The "first" refers to what kind of things we can quantify over.

In first-order logic, quantifiers range over *terms*

The W1 two-layer cake:
  - the term layer   1+3      x        x-(3*5)
           (no logic happening)
  - the wffs
        ⊤    1+4 ≤ 3    ∀x. x + 5 = 3

Variables always range over terms.

  ∀x. x+3 > 4

  counts as first-order because the quantifier ranges over
  a term.

(Not in this course)
Second-order logic:
  variables may range over *predicates about terms*

  ∀P. (P(0) ∧ (∀n. P(n) ⇒ P(n+1))) ⇒ ∀n. P(n)

   ^ it's the principle of basic induction!

  One of the main limitations of FOL:
   it can't do induction :(
   but you can still fake it enough to be useful :)

Also: you can't do a set comprehension :(

   {x | P(x)}


 ∀x y. x = y

is syntactic sugar for

 ∀x.(∀y. x = y)

When you use FOL, you will often specify
 the *domain of discourse*:
 the set of things you're talking about.

E.g., often domain is ℕ in our examples.

What if the domain of discourse is a
 singleton set {c}

 In other words: there's only thing in
  the world (as we model) it, and it's c.

In such a world, it is in fact true that
  ∀x y. x = y

 (philosophers and theologians have a name
  for such silly worlds: monism)

Q: If the domain is ∅, does that universal
   quantifiers are vacuously true?
A: We don't allow empty domains,
    but if did: then yes.

 By ruling out empty domains,
  we get a whole bunch of algebraic
  laws that would otherwise be invalid.


    ∃x. P    ≡  P     if x ∉ FV(P)

  ^ valid in non-empty domains,
    but not in empty domains